COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "let.pub" source
C00008 ENDMK
C⊗;
.require "let.pub" source
.at "Goedel" ⊂"G%C:%*odel"⊃
.font E "math30"
.at "qw" ⊂"%ET%*"⊃
∂AIL Dr. Patrick Hayes↓Department of Computer Science
↓University of Essex↓P.O. Box 23↓Wivenhoe Park↓Colchester↓England CO4 3SQ∞
Dear Pat:

	Thanks for your long letter.

	First, as you will see minimal inference is unrelated to optimal
fixed points.  I am rather skeptical about optimal fixed points, because
the optimal fixed point depends on the algebraic structure of the
computation space.  Thus extending the space from the integers to Gaussian
integers or %2R(%E\%12)
can change the optimal fixed point, and
therefore it is hard to see that the optimal fixed point represents
any kind of computational process.

	I can't just write down the functional equation
of %2occur%1 as an ordinary predicate, because I want to be able
to go from a recursive definition to its representation in
first order logic without having to prove anything
first.  I intend to do the proving
after getting into first order logic.  Therefore, whatever I can do
with %2occur%1, I must also be able to do with

	%Bsillier x ← ¬ sillier x%1,

but allowing

	%B∀x.(sillier x ≡ ¬sillier x)%1

is disastrous, because from it I can prove anything, i.e. the functional
equation has no interpretations at all.  However,

	%B∀x.(silliera x = not silliera x)%1

is entirely harmless.  Since we limit ourselves to continuous functionals,
solutions always exist.  By the way, you may be interested in
the enclosed note on strange continuous functionals.
.xgenlines←xgenlines-2

	You are right about equation 12, and I fixed it so that it now
corresponds to equation 13 at the cost of repeating the formula
that begins %2∃w%1.  My description operator is not exactly
Russell's, I guess, but I didn't invent it.  Tarski or somebody uses
one that has a conventional value when the desired %2x%1 doesn't
exist or isn't unique.  It isn't a minimization operator and can
always be eliminated from a sentence at the cost of making
the sentence longer.  The fact,
due, as I said, to Goedel and Kleene, that recursive
functions can be represented non-recursively is indeed surprising.
It is noteworthy that LISP permits stating these results more
compactly and concretely, and this appears also to be true of the
systems P, Q, and R of Tarski, Mostowski and Robinson %2Undecideable
Theories%1.  There will be more on this is the next version of this
paper which I will send you.

	I think Kowalski has a good idea in his first order logic
programming, but I am not yet sure what the idea is good for.
I have a paper from Keith Clark which seems to make sense.  What
I gather from that paper is that Kowalski's idea may permit a
smooth process of generating a program from a first order description
of the object to be computed by replacing non-computable constructions
a step at a time.

	I am now ethusiastic about the idea, used in the paper,
of imbedding three-valued logic in classical logic at the cost
of a separate domain of truth-values and another set of logical
connectives.  By paying this small price, I can say everything
I want, the semantics is clear, and the proofs seem to be straightforward.
When you read the %2concepts%1 paper, you will see that I also use
an extra set of connectives - this time for combining propositions.
There is yet another set used in my so far unwritten work on
extensional forms.  Incidentally, I am dubious about corner quotes
preferring ordinary quotes with explicit use of %2subst%1 when
variables are to be injected.

	I look forward to your reactions to the other papers.

.reg